i:Id, T:Type, ds:x:Id fp Type, P:(State(ds)TProp).
Normal(T)
 Normal(ds)
 (s:State(ds). Dec(v:T. P(s,v)))
 es.@i Precondition for "a"(v)
 es.@i P State(ds) (v:T) 

latex

Definitions	Id, P  Q, x:A. B(x), es.P(es), x:A. B(x), "$x", Prop, x. t(x), t  T, x(s)
Lemmas	normal-ds wf, normal-type wf, decidable wf, Rpre wf, R-pre-rule, Id wf, decl-state wf, fpf wf, event system wf, pre-p wf, R-realizes wf